$\forall$$D$:Dsys, $i$:Id, $k$:Knd.
\\[0ex]($\forall$$l$:IdLnk, ${\it tg}$:Id. M(source($l$)).dout($l$,${\it tg}$) $\subseteq\rho$ M(destination($l$)).din($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ (d{-}decl($D$;$i$)($k$)) $\subseteq\rho$ M($i$).da($k$)